A:Type, eq:EqDecider(A), f,g:fpf(A; a.top), x:A, z:top.
sqequal(fpf-cap(fpf-join(eq; f; g); eq; x; z);
sqequal(if fpf-dom(eq; x; f) then fpf-cap(f; eq; x; z) else fpf-cap(g; eq; x; z) fi ) 

latex

Definitions	x:A. B(x), top, fpf-cap(f; eq; x; z), if b then t else f fi , t  T, x. t(x), P  Q, tt, b, ff, b, prop{i:l}, P  Q, guard(T), , x(s), Unit, P  Q, P  Q, False, A,
Lemmas	fpf-join-ap-sq, fpf-dom wf, fpf-join wf, bool wf, eqtt to assert, btrue wf, eqff to assert, iff transitivity, assert wf, bnot wf, not wf, assert of bnot, fpf-join-dom, not functionality wrt iff, top wf, fpf wf, deq wf